@i: k affects only L
== e@i.
== kind(e) = k
==  (x:Id. ((x after e) = (x when e)  (x  L)) & ((x  L)  (x after e) = (x when e))) 

latex

---

clarification:

aframe-p(es;i;k;L)
== alle-at(es;i;e.es-kind(es; e) = k  Knd
== alle-at(es;i;e. (x:Id.
== alle-at(es;i;e. ((es-after(es; x; e) = es-when(es; x; e)  es-vartype(es; i; x)
== alle-at(es;i;e. (( (x  L  Id))
== alle-at(es;i;e. (& ((x  L  Id)
== alle-at(es;i;e. (& ( es-after(es; x; e) = es-when(es; x; e)  es-vartype(es; i; x)))) 

latex

Definitions	e@i. P(e), Knd, kind(e), x:A. B(x), P & Q, P  Q, A, (x  l), Id, s = t, vartype(i;x), (x after e), x when e
FDL editor aliases	aframe-p